a:, n:. 0  i < n. a  i = if qeq(a;1) then n else (1 - a  n/1 - a) fi    

latex

Definitions

r - s, (i = j), qeq(r;s), b, (r/s), r + s, A, r * s, P & Q, i  j < k, {i..j}, True, T, x. t(x), P  Q, P  Q, , ff, tt, P  Q, if b then t else f fi , , t  T, x:A. B(x), False, x(s), Unit, , , S  T

Lemmas

qmul comm qrng, qmul assoc qrng, qmul over minus qrng, qmul over plus qrng, qmul inv l, qinv wf, qadd assoc, mon ident q, qinv inv q, qexp wf, qmul assoc, qdiv wf, qmul wf, qadd wf, qmul one qrng, qsum-const, le wf, qexp-one, int seg wf, true wf, squash wf, qsum wf, int-rational, not functionality wrt iff, assert of bnot, eqff to assert, assert-qeq, eqtt to assert, iff transitivity, not wf, bnot wf, assert wf, bool wf, int inc rationals, qeq wf2, rationals wf, nat wf, sum of geometric prog q